T:Type, P:(T), as:T List.
(a:T. (a  as) & P(a))
 hd(filter(a.P(a);as))  T & (hd(filter(a.P(a);as))  as) & P(hd(filter(a.P(a);as))) 

latex

Definitions	{T}, P  Q, P  Q, A & B, (x  l), x(s), x:A. B(x), False, Unit, P  Q, P & Q, hd(l), , Prop, b, P  Q, A, t  T, b, x:A. B(x)
Lemmas	assert wf, not wf, bnot wf, bool wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, nil member, l member wf, cons member